/**
 * 
 */
package gov.nasa.jpf.namc.listener;

import java.io.BufferedReader;
import java.io.InputStreamReader;
import java.net.URL;

import gov.nasa.jpf.ListenerAdapter;
import gov.nasa.jpf.jvm.JVM;
import gov.nasa.jpf.jvm.MethodInfo;
import gov.nasa.jpf.jvm.SystemState;
import gov.nasa.jpf.jvm.ThreadInfo;
import gov.nasa.jpf.jvm.bytecode.Instruction;
import gov.nasa.jpf.jvm.bytecode.VirtualInvocation;
import gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet;
import gov.nasa.jpf.report.Publisher;
import gov.nasa.jpf.search.Search;

/**
 * @author nermnv
 *
 */
public class NamcListener extends ListenerAdapter {

	@Override
	public void instructionExecuted(JVM vm) {
		Instruction insn = vm.getLastInstruction();
		ThreadInfo ti = vm.getLastThreadInfo();
		SystemState ss = vm.getSystemState();
		if (insn instanceof VirtualInvocation) {
	        VirtualInvocation callInsn = (VirtualInvocation)insn;
	        int objref = callInsn.getCalleeThis(ti);
	        MethodInfo callee = callInsn.getInvokedMethod();//callInsn.getInvokedMethod(ti, objref);
	        if( callee!=null && callee.getCompleteName().equals("java.net.URL.openStream()Ljava/io/InputStream;") ) {
//	        	ss.breakTransition();
	        	ss.setMandatoryNextChoiceGenerator(new ThreadChoiceFromSet("openStream" + ss.getId(), vm.getThreadList().getRunnableThreads(), true), "fail message");
	        }
	    }
		super.instructionExecuted(vm);
	}

	@Override
	public void executeInstruction(JVM vm) {
		super.executeInstruction(vm);
	}

	@Override
	public void threadStarted(JVM vm) {
		super.threadStarted(vm);
	}

	@Override
	public void threadWaiting(JVM vm) {
		super.threadWaiting(vm);
	}

	@Override
	public void threadNotified(JVM vm) {
		super.threadNotified(vm);
	}

	@Override
	public void threadInterrupted(JVM vm) {
		super.threadInterrupted(vm);
	}

	@Override
	public void threadScheduled(JVM vm) {
		super.threadScheduled(vm);
	}

	@Override
	public void threadBlocked(JVM vm) {
		super.threadBlocked(vm);
	}

	@Override
	public void threadTerminated(JVM vm) {
		super.threadTerminated(vm);
	}

	@Override
	public void classLoaded(JVM vm) {
		super.classLoaded(vm);
	}

	@Override
	public void objectCreated(JVM vm) {
		super.objectCreated(vm);
	}

	@Override
	public void objectReleased(JVM vm) {
		super.objectReleased(vm);
	}

	@Override
	public void objectLocked(JVM vm) {
		super.objectLocked(vm);
	}

	@Override
	public void objectUnlocked(JVM vm) {
		super.objectUnlocked(vm);
	}

	@Override
	public void objectWait(JVM vm) {
		super.objectWait(vm);
	}

	@Override
	public void objectNotify(JVM vm) {
		super.objectNotify(vm);
	}

	@Override
	public void objectNotifyAll(JVM vm) {
		super.objectNotifyAll(vm);
	}

	@Override
	public void gcBegin(JVM vm) {
		super.gcBegin(vm);
	}

	@Override
	public void gcEnd(JVM vm) {
		super.gcEnd(vm);
	}

	@Override
	public void exceptionThrown(JVM vm) {
		super.exceptionThrown(vm);
	}

	@Override
	public void exceptionBailout(JVM vm) {
		super.exceptionBailout(vm);
	}

	@Override
	public void exceptionHandled(JVM vm) {
		super.exceptionHandled(vm);
	}

	@Override
	public void choiceGeneratorRegistered(JVM vm) {
		super.choiceGeneratorRegistered(vm);
	}

	@Override
	public void choiceGeneratorSet(JVM vm) {
		//System.out.println("choiceGeneratorSet   : " + vm.getChoiceGenerator().toString());
		//System.out.println("choiceGeneratorSet id: " + vm.getChoiceGenerator().getId());
		super.choiceGeneratorSet(vm);
	}

	@Override
	public void choiceGeneratorAdvanced(JVM vm) {
		//System.out.println("choises count: " + vm.getChoiceGenerator().getTotalNumberOfChoices());
		//System.out.println("CG   : " + vm.getChoiceGenerator().toString());
		//System.out.println("CG id: " + vm.getChoiceGenerator().getId());
		super.choiceGeneratorAdvanced(vm);
	}

	@Override
	public void choiceGeneratorProcessed(JVM vm) {
		super.choiceGeneratorProcessed(vm);
	}

	@Override
	public void methodEntered(JVM vm) {
		super.methodEntered(vm);
	}

	@Override
	public void methodExited(JVM vm) {
		super.methodExited(vm);
	}

	@Override
	public void stateAdvanced(Search search) {
		System.out.println("---------- stateAdvanced ----------");
		super.stateAdvanced(search);
	}

	@Override
	public void stateProcessed(Search search) {
		super.stateProcessed(search);
	}

	@Override
	public void stateBacktracked(Search search) {
		int id = search.getStateId();
	    System.out.println("----------------------------------- [" +
	                       search.getDepth() + "] backtrack: " + id);
	    
		try {
			URL url = new URL(search.getConfig().getString("resetServerUrl"));
			System.out.println((new BufferedReader(new InputStreamReader( url.openStream()))).readLine());
		} catch (Exception e) {
			e.printStackTrace();
		}
		super.stateBacktracked(search);
	}

	@Override
	public void statePurged(Search search) {
		super.statePurged(search);
	}

	@Override
	public void stateStored(Search search) {
		super.stateStored(search);
	}

	@Override
	public void stateRestored(Search search) {
		super.stateRestored(search);
	}

	@Override
	public void propertyViolated(Search search) {
		super.propertyViolated(search);
	}

	@Override
	public void searchStarted(Search search) {
		super.searchStarted(search);
	}

	@Override
	public void searchConstraintHit(Search search) {
		super.searchConstraintHit(search);
	}

	@Override
	public void searchFinished(Search search) {
		super.searchFinished(search);
	}

	@Override
	public void publishStart(Publisher publisher) {
		super.publishStart(publisher);
	}

	@Override
	public void publishTransition(Publisher publisher) {
		super.publishTransition(publisher);
	}

	@Override
	public void publishPropertyViolation(Publisher publisher) {
		super.publishPropertyViolation(publisher);
	}

	@Override
	public void publishConstraintHit(Publisher publisher) {
		super.publishConstraintHit(publisher);
	}

	@Override
	public void publishFinished(Publisher publisher) {
		super.publishFinished(publisher);
	}

}
